perm filename RAMSEY.NCI[EKL,SYS] blob
sn#860115 filedate 1988-08-18 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00019 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00003 00002 Divide and conquer....
C00008 00003 Proof and Interpretation in Direct Logic. Base Case, 1
C00011 00004 Interpretation of Base Case, 1:
C00013 00005 Now write the interpreted assumptions
C00015 00006 Interpretation of Base Case, 1:
C00016 00007 now do the interpretation
C00019 00008 Proof and Interpretation in Direct Logic. Base Case, 2.
C00022 00009 Interpretation of Base Case, 2:
C00023 00010 Now write the interpreted assumptions
C00027 00011 Interpretation of Base Case, 2:
C00028 00012 now do the interpretation
C00032 00013 Interpretation of Base Case, Conclusion.
C00041 00014 garbage collection: sketches for part 3
C00042 00015 (proof parttwoone)
C00059 00016 (proof parttwotwo)
C00071 00017 time used: 415 ms
C00084 00018 more sketches
C00087 00019 (setq der-slow t)
C00092 ENDMK
C⊗;
;;;Divide and conquer....
;(setq der-veryfast t)
;(fload padua)
(ekl)
(wipe-out)
(get-proofs natset prf ekl sys)
(proof declarations)
(decl (hf) (type: |ground⊗ground→ground|))
(decl Stab1 (type: |ground→@set|))
(decl stabf (type: |ground→ground|))
(axiom |∀x y.natnum(max(x,y))|)
(label simpinfo)
(axiom |∀n1 n2.n1<(max(n1,n2)') ∧ n2<(max(n1,n2)')|)
(label max)
(axiom |∀n i.¬(max(i,n)<n) ∧ ¬(max(i,n)<i)|)
(label max0)
(axiom |∀n1 n2 n3.max(n1,n2)<n3⊃n1<n3∧n2<n3|)
(label max3)
(assume |∀n3 n4.hf(n3,n4)=0∨hf(n3,n4)=1|)
(label a)
;;;specify the sort of Herbrand functions
(decl (mm1 jj1) (type: |ground→ground|) (sort: |natfunction|))
(decl (mm) (type: |ground⊗ground→ground|) (sort: |natfunction2|))
(axiom |∀f.natfunction(f)≡(∀x.natnum(f(x)))|)
;(axiom |∀f.natfunction(f)≡(∀n5.natnum(f(n5)))|)
(label natfunction)
;(ue (f |λx.mm1(x)|) natfunction)
;∀X.NATNUM(MM1(X))
;(ue (x |KKK1(jj1,mm1,i)|) *)
;(label temp)
(axiom |∀f2.natfunction2(f2)≡(∀x y.natnum(f2(x,y)))|)
;(axiom |∀f2.natfunction2(f2)≡(∀n6 n7.natnum(f2(n6,n7)))|)
(label natfunction2)
(derive |∀mm n8 n9.natnum(mm[n8,n9])| natfunction2)
(label simpinfo)
(derive |∀mm1 n10.natnum(mm1[n10])| (natfunction))
(label simpinfo)
;;Proof and Interpretation in Direct Logic. Base Case, 1
(proof partoneone)
(derive |∀n.hf(0,max(n,i)')=0∨hf(0,max(n,i)')=1| a)
(label a1)
(assume |¬(∀j.∃K0.hf(0,K0)=0∧j<K0)|)
(label b1)
(assume |∀N.¬(∀K1.∃m.hf(0,m)=0∧k1<m) ⊃ (hf(0,N)=1⊃NεStab1(0))|)
(label c1)
(derive |∃J.JεStab1(0)∧i<J| (max a1 b1 b1 c1))
(label d1)
;deps: (A B1 C1)
(ci (b1 c1))
;¬(∀J.(∃K0.HF(0,K0)=0∧J<K0))∧(∀N.HF(0,N)=1⊃NεSTAB1(0))⊃(∃J.JεSTAB1(0)∧I<J)
(label concl1)
;deps: (A)
(ci (c1) 4 )
;(∀N.¬(∀K1.(∃M.HF(0,M)=0∧K1<M))⊃(HF(0,N)=1⊃NεSTAB1(0))⊃(∃J.JεSTAB1(0)∧I<J)
;deps: (A B1)
(derive
|(∀N. (∀J1.(∃K.hf(0,K)=0∧J1<K))⊃(hf(0,N)=0⊃NεStab1(0)))∧
(∀N.¬(∀K1.(∃M.hf(0,M)=0∧K1<M))⊃(hf(0,N)=1⊃NεStab1(0)))⊃(∃J.JεStab1(0)∧I<J)| *)
(label conclude1)
;deps: (A B1)
;;;;;;;;;;;;;;;;
;IT WORKS
;after finding a path
;path:
;J<K0 from hf(0,K0)=0∧J<K0 :: ¬N1<MAX(N1,N2)' from ¬N1<MAX(N1,N2)'
;I<J from JεStab1(0)∧I<J :: ¬N2<MAX(N1,N2)' from ¬N2<MAX(N1,N2)'
;hf(0,K0)=0 from hf(0,K0)=0∧J<K0 :: ¬hf(0,M)=0 from (****∨¬hf(0,M)=0∨¬K1<M)∧hf(0,N)=1∧¬NεStab1(0)
;hf(0,K0)=0 from hf(0,K0)=0∧J<K0 :: ¬hf(0,MAX(N,I)')=0 from ¬hf(0,MAX(N,I)')=0∧¬hf(0,MAX(N,I)')=1
;JεStab1(0) from JεStab1(0)∧I<J :: ¬NεStab1(0) from (****∨¬hf(0,M)=0∨¬K1<M)∧hf(0,N)=1∧¬NεStab1(0)
;J<K0 from hf(0,K0)=0∧J<K0 :: ¬K1<M from (****∨¬hf(0,M)=0∨¬K1<M)∧hf(0,N)=1∧¬NεStab1(0)
;hf(0,N)=1 from (****∨¬hf(0,M)=0∨¬K1<M)∧hf(0,N)=1∧¬NεStab1(0) :: ¬hf(0,MAX(N,I)')=1
;from ¬hf(0,MAX(N,I)')=0∧¬hf(0,MAX(N,I)')=1
;bound in variable CTR85
;unifier: ((N . J) (I . I) (N2 . I) (N1 . J) (K0 . MAX(J,I)') (J . MAX(J,I)')
;(N . MAX(J,I)') (K0 . M(J,MAX(J,I)')) (K1 . J))
;deps: (A B1 C1)
;;;Interpretation of Base Case, 1:
;;;define functionals from the unifiers
;unifier: ((N . J) (I . I) (N2 . I) (N1 . J) (K0 . MAX(J,I)') (J . MAX(J,I)')
(N . MAX(J,I)') (K0 . M(J,MAX(J,I)')) (K1 . J))
(proof partoneone_kreisel)
(define KKK00 |(KKK00=λj i.max(j,i)')|)
(label KKK00def)
(define KKK01 |(KKK01=λmm j i.mm(max(j,i)',j))|)
(label KKK01def)
(define KKK2 |(KKK2=λj.j)|)
(label KKK2def)
(define NNN1 |NNN1 = λj i.max(j,i)'|)
(label NNN1def)
(define JJJ1 |JJJ1 = λj i.max(j,i)'|)
(label JJJ1def)
;;;;(trw |∀j i.natnum (KKK00(j,i))| (open kkk00))
;;;;PDL OVERFLOW;
(axiom |∀j i.natnum (KKK00(j,i))|)
(label simpinfo)
(axiom |∀mm j i.natnum (KKK01(mm,j,i))|)
(label simpinfo)
;Now write the interpreted assumptions
(assume |¬(hf(0,KKK00(j,i))=0∧j<KKK00(j,i))|)
(label bk00)
(assume |¬(hf(0,KKK01(mm,j,i))=0∧j<KKK01(mm,j,i))|)
(label bk01)
(assume |¬(hf(0,mm[NNN1(j,i),KKK2(j)])=0∧KKK2(j)<mm[NNN1(j,i),KKK2(j)]) ⊃
(hf(0,NNN1(j,i))=1⊃NNN1(j,i)εStab1(0) )|)
(label ck1)
;now rewrite the functionals and obtain the skeleton
(rw bk00 (open kkk00) max)
(label be00)
;¬HF(0,MAX(J,I)')=0
(rw bk01 (open kkk01))
(label be01)
;¬(HF(0,MM(MAX(J,I)',J))=0∧J<MM(MAX(J,I)',J))
;deps: (BK01)
(rw ck1 (open nnn1 kkk2))
(label ce01)
;¬(HF(0,MM(MAX(J,I)',J))=0∧J<MM(MAX(J,I)',J))⊃
;(HF(0,MAX(J,I)')=1⊃MAX(J,I)'εSTAB1(0))
;deps: (CK1)
;derive the interpretation of the conclusion
(ue ((n3.|0|)(n4.|max(j,i)'|)) a be00)
;HF(0,MAX(J,I)')=1
;deps: (A BK00)
(trw |JJJ1(j,i)εStab1(0)∧i<JJJ1(j,i)|
(use max * be01 ce01) (open JJJ1))
;JJJ1(J,I)εSTAB1(0)∧I<JJJ1(J,I)
(label dk1)
;deps: (A BK00 BK01 CK1)
(ci (bk00 bk01 ck1) )
;¬(HF(0,KKK00(J,I))=0∧J<KKK00(J,I))∧¬(HF(0,KKK01(MM,J,I))=0∧J<KKK01(MM,J,I))∧
;(¬(HF(0,MM(NNN1(J,I),KKK2(J)))=0∧KKK2(J)<MM(NNN1(J,I),KKK2(J)))⊃
; (HF(0,NNN1(J,I))=1⊃NNN1(J,I)εSTAB1(0)))⊃JJJ1(J,I)εSTAB1(0)∧I<JJJ1(J,I)
(label conclk1)
;deps: (A)
;;;Interpretation of Base Case, 1:
;;introduce contractions in the interpretation
(proof full_partone_kreisel)
;conditional term to interpret a contraction
(define KKK0 |KKK0 = (λmm j i.
if hf(0,KKK00(J,I))=0∧J<KKK00(J,I)
then KKK00(j,i)
else KKK01(mm,j,i))|)
(axiom |∀mm j i.natnum(KKK0(mm,j,i))|)
(label simpinfo)
;now do the interpretation
(assume |¬(hf(0,KKK0(mm,j,i))=0∧j<KKK0(mm,j,i))|)
(label bkc0)
(rw bkc0 (open KKK0))
;¬((HF(0,KKK00(J,I))=0∧J<KKK00(J,I)∨HF(0,KKK01(MM,J,I))=0)∧
; (HF(0,KKK00(J,I))=0∧J<KKK00(J,I)∨J<KKK01(MM,J,I)))
;deps: (BKC0)
(derive |¬(hf(0,KKK00(J,I))=0∧J<KKK00(J,I))∧
¬(hf(0,KKK01(MM,J,I))=0∧J<KKK01(MM,J,I))| *)
;deps: (BKC0)
(rw * (open KKK00 KKK01))
;¬(HF(0,MAX(J,I)')=0∧J<MAX(J,I)')∧
;¬(HF(0,MM(MAX(J,I)',J))=0∧J<MM(MAX(J,I)',J))
;deps: (BKC0)
;the assumption of this part, fully evaluated
(rw * max)
;¬HF(0,MAX(J,I)')=0∧¬(HF(0,MM(MAX(J,I)',J))=0∧J<MM(MAX(J,I)',J))
;deps: (BKC0)
(label bkce0)
;cl is a bicolorig
(ue ((n3.|0|)(n4.|max(j,i)'|)) a bkce0)
;HF(0,MAX(J,I)')=1
(label ake0)
;deps: (A BKC0)
;the definition of Stab1(0)
(rw ck1 (open nnn1 kkk2))
;(label ce01)
;¬(HF(0,MM(MAX(J,I)',J))=0∧J<MM(MAX(J,I)',J))⊃
;(HF(0,MAX(J,I)')=1⊃MAX(J,I)'εSTAB1(0))
;deps: (CK1)
(rw * bkce0 ake0)
;MAX(J,I)'εSTAB1(0)
;deps: (A CK1 BKC0)
(trw |JJJ1(j,i)εStab1(0)∧i<JJJ1(j,i)|
(use max *) (open JJJ1))
;JJJ1(j,i)εStab1(0)∧I<JJJ1(J,I)
;JJJ1(J,I)εSTAB1(0)∧I<JJJ1(J,I)
;deps: (A CK1 BKC0)
(ci (ck1 bkc0))
;(¬(HF(0,MM(NNN1(J,I),KKK2(J)))=0∧KKK2(J)<MM(NNN1(J,I),KKK2(J)))⊃
; (HF(0,NNN1(J,I))=1⊃NNN1(J,I)εSTAB1(0)))∧
;¬(HF(0,KKK0(MM,J,I))=0∧J<KKK0(MM,J,I))⊃JJJ1(J,I)εSTAB1(0)∧I<JJJ1(J,I)
(label conclkc1)
;deps: (A)
;;Proof and Interpretation in Direct Logic. Base Case, 2.
(proof partonetwo)
(assume |∀K1.∃m.hf(0,m)=0∧k1<m|)
(label b2)
(assume |∀N.(∀j1.∃K.hf(0,K)=0∧j1<K) ⊃ (hf(0,N)=0⊃NεStab1(0))|)
(label c2)
(derive |∃J.JεStab1(0)∧i<J| (b2 b2 c2))
(label d2)
;deps: (B2 C2)
(ci (b2 c2))
;(∀K1.(∃M.HF(0,M)=0∧K1<M))∧(∀N.HF(0,N)=0⊃NεSTAB1(0))⊃(∃J.JεSTAB1(0)∧I<J)
(label concl2)
(ci c2 3)
;(∀N.(∀J1.(∃K.HF(0,K)=0∧J1<K))⊃(HF(0,N)=0⊃NεSTAB1(0)))⊃(∃J.JεSTAB1(0)∧I<J)
;deps: (B2)
(derive
|(∀N.(∀J1.(∃K.hf(0,K)=0∧J1<K))⊃(hf(0,N)=0⊃NεStab1(0)))∧
(∀N.¬(∀K1.(∃M.hf(0,M)=0∧K1<M))⊃(hf(0,N)=1⊃NεStab1(0)))⊃(∃J.JεStab1(0)∧I<J)| *)
;deps: (B2)
(label conclude2)
;;;;;;;;;;;;;;;;
;IT WORKS
;time used: 334 ms
;after initialisation
;....
;after finding a path
;path:
;I<J from JεStab1(0)∧I<J :: ¬K1<M from ¬K1<M
;JεStab1(0) from JεStab1(0)∧I<J :: ¬NεStab1(0) from (****∨hf(0,K)=0∧J1<K)∧hf(0,N)=0∧¬NεStab1(0)
;hf(0,N)=0 from (****∨hf(0,K)=0∧J1<K)∧hf(0,N)=0∧¬NεStab1(0) :: ¬hf(0,M)=0 from
¬hf(0,M)=0
;hf(0,K)=0 from (****∨hf(0,K)=0∧J1<K)∧hf(0,N)=0∧¬NεStab1(0) :: ¬hf(0,M)=0 from
¬hf(0,M)=0
;J1<K from (****∨hf(0,K)=0∧J1<K)∧hf(0,N)=0∧¬NεStab1(0) :: ¬K1<M from ¬K1<M
;bound in variable CTR51
;unifier: ((K1 . I) (J . M(I)) (N . M(I)) (K . M(J1(M(I)))) (K1 . J1(M(I))))
;deps: (B2 C2)
;;Interpretation of Base Case, 2:
;;define the functionals from the unifiers
;unifier: ((K1 . I) (J . M(I)) (N . M(I)) (K . M(J1(M(I)))) (K1 . J1(M(I))))
(proof partonetwo_kreisel)
(define KKK11 |(KKK11 = λi.i)|)
(label kkk11def)
(define KKK12 |(KKK12 = λjj1 mm1 i.jj1(mm1(i)))|)
(label kkk12def)
(define NNN3 |(NNN3 = λmm1 i.mm1(i))|)
(label nnn3def)
(define KKK3 |(KKK3 = λmm1 jj1 i.mm1(jj1(mm1(i))))|)
(label kkk3def)
(define JJJ3 |(JJJ3 = λmm1 i.mm1(i))|)
(label jjj3def)
(trw |∀i.natnum(KKK11(I))| (open KKK11))
;∀I.NATNUM(KKK11(I))
(label simpinfo)
;Now write the interpreted assumptions
(assume |hf(0,mm1[KKK11(i)])=0∧KKK11(i)<mm1[KKK11(i)]|)
(label bk2)
(assume |hf(0,mm1[KKK12(jj1,mm1,i)])=0∧KKK12(jj1,mm1,i)<mm1[KKK12(jj1,mm1,i)]|)
(label bk3)
(assume |(hf(0,KKK3(mm1,jj1,i))=0∧jj1[NNN3(mm1,i)]<KKK3(mm1,jj1,i)) ⊃
(hf(0,NNN3(mm1,i))=0⊃NNN3(mm1,i)εStab1(0) )|)
(label ck2)
;now rewrite the functionals and obtain the skeleton
(rw bk2 (open kkk11))
;HF(0,MM1(I))=0∧I<MM1(I)
(label be2)
(rw bk3 (open kkk12))
(label be3)
;HF(0,MM1(JJ1(MM1(I))))=0∧JJ1(MM1(I))<MM1(JJ1(MM1(I)))
;deps: (BK3)
(rw ck2 (open kkk3 nnn3))
;HF(0,MM1(JJ1(MM1(I))))=0∧JJ1(MM1(I))<MM1(JJ1(MM1(I)))⊃
;(HF(0,MM1(I))=0⊃MM1(I)εSTAB1(0))
(label ce2)
;deps: (CK2)
;derive the interpretation of the conclusion
(derive |JJJ3(mm1,i)εStab1(0)∧i<JJJ3(mm1,i)| (be2 be3 ce2) (open jjj3))
;deps: (BK2 BK3 CK2)
(ci (bk2 bk3 ck2))
;HF(0,MM1(KKK11(I)))=0∧KKK11(I)<MM1(KKK11(I))∧HF(0,MM1(KKK12(JJ1,MM1,I)))=0∧
;KKK12(JJ1,MM1,I)<MM1(KKK12(JJ1,MM1,I))∧
;(HF(0,NNN3(MM1,I))=0⊃NNN3(MM1,I)εSTAB1(0))⊃JJJ3(MM1,I)εSTAB1(0)∧I<JJJ3(MM1,I)
(label conclk2)
;;Interpretation of Base Case, 2:
;;introduce contractions in the interpretation
(proof full_partone_kreisel)
;conditional term to interpret a contraction
(define KKK1 |KKK1 = (λjj1 mm1 i.
if ¬(hf(0,mm1[KKK11(i)])=0∧KKK11(i)<mm1[KKK11(i)])
then KKK11(i)
else KKK12(jj1,mm1,i))|)
(axiom |∀jj1 mm1 i.natnum(KKK1(jj1,mm1,i))|)
(label simpinfo)
;now do the interpretation
(assume |hf(0,mm1[KKK1(jj1,mm1,i)])=0∧KKK1(jj1,mm1,i)<mm1[KKK1(jj1,mm1,i)]|)
(label bkc1)
(rw bkc1 (open KKK1))
;(IF ¬(HF(0,MM1(KKK11(I)))=0∧KKK11(I)<MM1(KKK11(I))) THEN HF(0,MM1(KKK11(I)))=0
; ELSE HF(0,MM1(KKK12(JJ1,MM1,I)))=0)∧
;(IF ¬(HF(0,MM1(KKK11(I)))=0∧KKK11(I)<MM1(KKK11(I)))
; THEN KKK11(I)<MM1(KKK11(I)) ELSE KKK12(JJ1,MM1,I)<MM1(KKK12(JJ1,MM1,I)))
;deps: (BKC1)
(assume |¬(hf(0,MM1(KKK11(I)))=0∧KKK11(I)<MM1(KKK11(I)))|)
;deps: (5)
(rw -2 *)
;FALSE
;FALSE
;deps: (17 BKC1)
(ci -2)
;HF(0,MM1(KKK11(I)))=0∧KKK11(I)<MM1(KKK11(I))
(label bkc11)
;deps: (BKC1)
(rw -4 *)
;HF(0,MM1(KKK12(JJ1,MM1,I)))=0∧KKK12(JJ1,MM1,I)<MM1(KKK12(JJ1,MM1,I))
(label bkc12)
;deps: (BKC1)
;now fully evaluate the assumption of this part
(rw bkc11 (open KKK11))
;HF(0,MM1(I))=0∧I<MM1(I)
(label bkce11)
;deps: (BKC1)
(rw bkc12 (open KKK12))
;HF(0,MM1(JJ1(MM1(I))))=0∧JJ1(MM1(I))<MM1(JJ1(MM1(I)))
(label bkce12)
;deps: (BKC1)
(assume |(hf(0,KKK3(mm1,jj1,i))=0∧jj1[NNN3(mm1,i)]<KKK3(mm1,jj1,i)) ⊃
(hf(0,NNN3(mm1,i))=0⊃NNN3(mm1,i)εStab1(0) )|)
(label ck2)
(rw * (open kkk3 nnn3))
;HF(0,MM1(JJ1(MM1(I))))=0∧JJ1(MM1(I))<MM1(JJ1(MM1(I)))⊃
;(HF(0,MM1(I))=0⊃MM1(I)εSTAB1(0))
(label ce2)
;deps: (CK2)
(derive |JJJ3(mm1,i)εStab1(0)∧i<JJJ3(mm1,i)| (bkce11 bkce12 ce2) (open jjj3))
;deps: (CK2 BKC1)
(ci (bkc1 ck2))
;HF(0,MM1(KKK1(JJ1,MM1,I)))=0∧KKK1(JJ1,MM1,I)<MM1(KKK1(JJ1,MM1,I))∧
;(HF(0,KKK3(MM1,JJ1,I))=0∧JJ1(NNN3(MM1,I))<KKK3(MM1,JJ1,I)⊃
; (HF(0,NNN3(MM1,I))=0⊃NNN3(MM1,I)εSTAB1(0)))⊃
;JJJ3(MM1,I)εSTAB1(0)∧I<JJJ3(MM1,I)
(label conclkc2)
;;Interpretation of Base Case, Conclusion.
(proof end_partone_kreisel)
(define JJJ |JJJ = (λmm jj1 i.
if JJJ1(KKK1(jj1,λx.KKK0(mm,x,i),i),i)εStab1(0)∧
I<JJJ1(KKK1(jj1,λx.KKK0(mm,x,i),i),i)
then JJJ1(KKK1(jj1,λx.KKK0(mm,x,i),i),i)
else JJJ3(λx.KKK0(mm,x,i),i) )|)
(axiom |∀mm jj1 i.natnum(JJJ(mm,jj1,i))|)
(label simpinfo)
(axiom |natfunction(λx.KKK0(mm,x,i))|)
(label simpinfo)
(axiom |natnum(kkk1(jj1,λx.KKK0(mm,x,i),i))|)
(label simpinfo)
;;;;these were proved in the proof full_partone_kreisel
(axiom |∀mm j i.¬(hf(0,KKK0(mm,j,i))=0∧J<KKK0(mm,j,i)) ⊃
[(¬(hf(0,mm(NNN1(j,i),KKK2(j)))=0∧KKK2(j)<mm(NNN1(j,i),KKK2(j)))⊃
(hf(0,NNN1(j,i))=1⊃NNN1(j,i)εStab1(0)))
⊃ JJJ1(j,i)εStab1(0)∧i<JJJ1(j,i)]|)
(label conclkc1)
(axiom |∀jj1 mm1 i.
hf(0,mm1(KKK1(jj1,mm1,i)))=0∧KKK1(jj1,mm1,i)<mm1(KKK1(jj1,mm1,i))⊃
[(hf(0,KKK3(mm1,jj1,i))=0∧jj1(NNN3(mm1,i))<KKK3(mm1,jj1,i)⊃
(hf(0,NNN3(mm1,i))=0⊃NNN3(mm1,i)εStab1(0)))
⊃ JJJ3(mm1,i)εStab1(0)∧i<JJJ3(mm1,i)]|)
(label conclkc2)
;;;now we make the appropriate substitutions for CUT
(ue ((mm.|mm|)(j.|kkk1(jj1,λx.KKK0(mm,x,i),i)|)(i.i)) conclkc1)
;¬(hf(0,KKK0(MM,KKK1(JJ1,λX.KKK0(MM,X,I),I),I))=0∧
; KKK1(JJ1,λX.KKK0(MM,X,I),I)<KKK0(MM,KKK1(JJ1,λX.KKK0(MM,X,I),I),I))⊃
;((¬(hf(0,
; MM(NNN1(KKK1(JJ1,λX.KKK0(MM,X,I),I),I),
; KKK2(KKK1(JJ1,λX.KKK0(MM,X,I),I))))=0∧
; KKK2(KKK1(JJ1,λX.KKK0(MM,X,I),I))<
; MM(NNN1(KKK1(JJ1,λX.KKK0(MM,X,I),I),I),
; KKK2(KKK1(JJ1,λX.KKK0(MM,X,I),I))))⊃
; (hf(0,NNN1(KKK1(JJ1,λX.KKK0(MM,X,I),I),I))=1⊃
; NNN1(KKK1(JJ1,λX.KKK0(MM,X,I),I),I)εStab1(0)))⊃
; JJJ1(KKK1(JJ1,λX.KKK0(MM,X,I),I),I)εStab1(0)∧
; I<JJJ1(KKK1(JJ1,λX.KKK0(MM,X,I),I),I))
(label interpreted_part01)
(ue ((mm1.|λx.KKK0(mm,x,i)|)(jj1.|jj1|)(i.i)) conclkc2)
;hf(0,KKK0(MM,KKK1(JJ1,λX.KKK0(MM,X,I),I),I))=0∧
;KKK1(JJ1,λX.KKK0(MM,X,I),I)<KKK0(MM,KKK1(JJ1,λX.KKK0(MM,X,I),I),I)⊃
;((hf(0,KKK3(λX.KKK0(MM,X,I),JJ1,I))=0∧
; JJ1(NNN3(λX.KKK0(MM,X,I),I))<KKK3(λX.KKK0(MM,X,I),JJ1,I)⊃
; (hf(0,NNN3(λX.KKK0(MM,X,I),I))=0⊃NNN3(λX.KKK0(MM,X,I),I)εStab1(0)))⊃
; JJJ3(λX.KKK0(MM,X,I),I)εStab1(0)∧I<JJJ3(λX.KKK0(MM,X,I),I))
(label interpreted_part02)
;;;appropriate abbreviations
(define interpreted_definition
|interpreted_definition
≡
(hf(0,KKK3(λX.KKK0(MM,X,I),JJ1,I))=0∧
JJ1(NNN3(λX.KKK0(MM,X,I),I))<KKK3(λX.KKK0(MM,X,I),JJ1,I)⊃
(hf(0,NNN3(λX.KKK0(MM,X,I),I))=0⊃NNN3(λX.KKK0(MM,X,I),I)εStab1(0)))
∧
(¬(hf(0,
MM(NNN1(KKK1(JJ1,λX.KKK0(MM,X,I),I),I),
KKK2(KKK1(JJ1,λX.KKK0(MM,X,I),I))))=0∧
KKK2(KKK1(JJ1,λX.KKK0(MM,X,I),I))<
MM(NNN1(KKK1(JJ1,λX.KKK0(MM,X,I),I),I),
KKK2(KKK1(JJ1,λX.KKK0(MM,X,I),I))))⊃
(hf(0,NNN1(KKK1(JJ1,λX.KKK0(MM,X,I),I),I))=1⊃
NNN1(KKK1(JJ1,λX.KKK0(MM,X,I),I),I)εStab1(0))) |)
(define interpreted_conclusion
|interpreted_conclusion
≡
JJJ1(KKK1(JJ1,λX.KKK0(MM,X,I),I),I)εStab1(0)∧
I<JJJ1(KKK1(JJ1,λX.KKK0(MM,X,I),I),I)
∨
JJJ3(λX.KKK0(MM,X,I),I)εStab1(0)∧I<JJJ3(λX.KKK0(MM,X,I),I)|)
;;;;the argument by cases is safely done in an interactive way
(assume |¬(hf(0,KKK0(MM,KKK1(JJ1,λX.KKK0(MM,X,I),I),I))=0∧
KKK1(JJ1,λX.KKK0(MM,X,I),I)<KKK0(MM,KKK1(JJ1,λX.KKK0(MM,X,I),I),I))|)
(label caseone)
(rw interpreted_part01 caseone)
;(¬(hf(0,
; MM(NNN1(KKK1(JJ1,λX.KKK0(MM,X,I),I),I),
; KKK2(KKK1(JJ1,λX.KKK0(MM,X,I),I))))=0∧
; KKK2(KKK1(JJ1,λX.KKK0(MM,X,I),I))<
; MM(NNN1(KKK1(JJ1,λX.KKK0(MM,X,I),I),I),KKK2(KKK1(JJ1,λX.KKK0(MM,X,I),I))))⊃
; (hf(0,NNN1(KKK1(JJ1,λX.KKK0(MM,X,I),I),I))=1⊃
; NNN1(KKK1(JJ1,λX.KKK0(MM,X,I),I),I)εStab1(0)))⊃
;JJJ1(KKK1(JJ1,λX.KKK0(MM,X,I),I),I)εStab1(0)∧I<JJJ1(KKK1(JJ1,λX.KKK0(MM,X,I),I),I)
;deps: (CASEONE)
(trw |interpreted_definition⊃interpreted_conclusion|
(open interpreted_definition interpreted_conclusion) *)
;INTERPRETED_DEFINITION⊃INTERPRETED_CONCLUSION
;deps: (CASEONE)
(assume |(hf(0,KKK0(MM,KKK1(JJ1,λX.KKK0(MM,X,I),I),I))=0∧
KKK1(JJ1,λX.KKK0(MM,X,I),I)<KKK0(MM,KKK1(JJ1,λX.KKK0(MM,X,I),I),I))|)
(label casetwo)
;deps: (15)
(rw interpreted_part02 casetwo)
;(hf(0,KKK3(λX.KKK0(MM,X,I),JJ1,I))=0∧
; JJ1(NNN3(λX.KKK0(MM,X,I),I))<KKK3(λX.KKK0(MM,X,I),JJ1,I)⊃
; (hf(0,NNN3(λX.KKK0(MM,X,I),I))=0⊃NNN3(λX.KKK0(MM,X,I),I)εStab1(0)))⊃
;JJJ3(λX.KKK0(MM,X,I),I)εStab1(0)∧I<JJJ3(λX.KKK0(MM,X,I),I)
;deps: (CASETWO)
(trw |interpreted_definition⊃interpreted_conclusion|
(open interpreted_definition interpreted_conclusion) *)
;INTERPRETED_DEFINITION⊃INTERPRETED_CONCLUSION
;deps: (CASETWO)
(derive |(hf(0,KKK0(MM,KKK1(JJ1,λX.KKK0(MM,X,I),I),I))=0∧
KKK1(JJ1,λX.KKK0(MM,X,I),I)<KKK0(MM,KKK1(JJ1,λX.KKK0(MM,X,I),I),I))
∨
¬(hf(0,KKK0(MM,KKK1(JJ1,λX.KKK0(MM,X,I),I),I))=0∧
KKK1(JJ1,λX.KKK0(MM,X,I),I)<KKK0(MM,KKK1(JJ1,λX.KKK0(MM,X,I),I),I))|)
(cases * -2 -5)
;INTERPRETED_DEFINITION⊃INTERPRETED_CONCLUSION
;;;Finally, we rewrite using the desired functional
(assume |interpreted_definition|)
(label closing)
(rw -2 closing (open interpreted_conclusion))
;JJJ1(KKK1(JJ1,λX.KKK0(MM,X,I),I),I)εStab1(0)∧
;I<JJJ1(KKK1(JJ1,λX.KKK0(MM,X,I),I),I)∨
;JJJ3(λX.KKK0(MM,X,I),I)εStab1(0)∧I<JJJ3(λX.KKK0(MM,X,I),I)
;deps: (CLOSING)
(derive |JJJ(mm,jj1,i)εStab1(0) ∧ i<JJJ(mm,jj1,i)| *
(open JJJ))
;deps: (CLOSING)
(ci closing)
;INTERPRETED_DEFINITION⊃JJJ(MM,JJ1,I)εStab1(0)∧I<JJJ(MM,JJ1,I)
;;;garbage collection: sketches for part 3
(proof parttwoone)
(assume |¬∀j.∃K0.K0εStab1(n)∧hf(n',K0)=0∧j<K0|)
(label b3)
(assume |∀N0.(¬∀K1.∃m.mεStab1(n)∧hf(n',m)=0∧k1<m) ⊃ (N0εStab1(n)∧hf(n',N0)=1⊃N0εStab1(n'))|)
(label c3)
(assume |∀k.∃m.mεStab1(n)∧k<m|)
(label d3)
(define e |¬(∃K0.K0εStab1(n)∧hf(n',K0)=0∧e<K0)∧natnum(e)| b3)
(label b31)
(define aa |(∀k.aa(k)εStab1(n)∧k<aa(k))∧∀k.natnum(aa(k))| d3)
;deps: (D3)
(ue (k |max(i,e)|) *)
;AA(MAX(I,E))εStab1(N)∧MAX(I,E)<AA(MAX(I,E))∧NATNUM(AA(MAX(I,E)))
(label d31)
;deps: (D3)
(ue (k0 |aa(max(i,e))|) b31 * max3)
;¬hf(N',AA(MAX(I,E)))=0∧NATNUM(E)
;deps: (B3 D3)
(ue ((m.|n'|)(n.|aa(max(i,e))|)) a d31 *)
;hf(N',AA(MAX(I,E)))=1
;deps: (A B3 D3)
(label a31)
(ue (n0 |aa(max(i,e))|) c3 b3 d31 a31)
;AA(MAX(I,E))εStab1(N')
;deps: (A B3 C3 D3)
(ue ((n1.i)(n2.e)(n3.|aa(max(i,e))|)) max3 d31 b31)
;I<AA(MAX(I,E))∧E<AA(MAX(I,E))
;deps: (B3 D3)
(derive |AA(MAX(I,E))εStab1(N')∧I<AA(MAX(I,E))∧natnum(aa(max(i,e)))| (-1 -2 d31))
;deps: (A B3 C3 D3)
(derive |∃J.JεStab1(n')∧i<J| *)
; failed to derive
∃J.JεStab1(N')∧I<J
;time used: 13 ms
;after initialisation
; facts: (¬NATNUM(I) ¬NATNUM(N) ¬AA(MAX(I,E))εStab1(N')
;¬I<AA(MAX(I,E)) ¬NATNUM(AA(MAX(I,E))) JεStab1(N')∧I<J)
;number of unifiable pairs: 2
;number of positive atoms: 2 and number of negative atoms: 5
;after first irrelevance elimination:
;time used: 5 ms
; facts: (¬AA(MAX(I,E))εStab1(N') ¬I<AA(MAX(I,E)) JεStab1(N')∧I<J)
;number of unifiable pairs: 2
;number of positive atoms: 2 and number of negative atoms: 2
;time used: 3 ms
;after primitive propagation
;0 combination failures.
; facts: (¬AA(MAX(I,E))εStab1(N') ¬I<AA(MAX(I,E)) JεStab1(N')∧I<J)
;number of unifiable pairs: 2
;number of positive atoms: 2 and number of negative atoms: 2
;time used: 0 ms
;after propagation
;0 combination failures.
; facts: (¬AA(MAX(I,E))εStab1(N') ¬I<AA(MAX(I,E)) JεStab1(N')∧I<J)
;number of unifiable pairs: 2
;number of positive atoms: 2 and number of negative atoms: 2
;time used: 1 ms
;after noncyclicity marking
;number of cyclic conjunctions found: 0
;top-level unifiers: (1 1 1)
;***
;uniflst for ¬AA(MAX(I,E))εStab1(N')
;***
;path:
;JεStab1(N') from JεStab1(N')∧I<J :: ¬AA(MAX(I,E))εStab1(N') from ¬AA(MAX(I,E))εStab1(N')
;unifier: ((J . AA(MAX(I,E))))
;***
;uniflst for ¬I<AA(MAX(I,E))
;***
;path:
;I<J from JεStab1(N')∧I<J :: ¬I<AA(MAX(I,E)) from ¬I<AA(MAX(I,E))
;unifier: ((J . AA(MAX(I,E))) (I . I))
;***
;uniflst for JεStab1(N')∧I<J
;***
;path:
;JεStab1(N') from JεStab1(N')∧I<J :: ¬AA(MAX(I,E))εStab1(N') from ¬AA(MAX(I,E))εStab1(N')
;I<J from JεStab1(N')∧I<J :: ¬I<AA(MAX(I,E)) from ¬I<AA(MAX(I,E))
;unifier: ((J . AA(MAX(I,E))) (I . I))
;time used: 7 ms
; failed to derive
∃J.JεStab1(N')∧I<J
(proof parttwotwo)
(assume |∀K1.∃m.mεStab1(n)∧hf(n',m)=0∧k1<m|)
(label b4)
(assume |∀n1.(∀j.∃k.kεStab1(n)∧hf(n',k)=0∧j<k) ⊃ (n1εStab1(n)∧hf(n',n1)=0⊃n1εStab1(n'))|)
(label c4)
(assume |∀k.∃m.mεStab1(n)∧k<m|)
(label d4)
(derive |∀i.∃J.JεStab1(n')∧i<J| (max0 a b4 b4 c4 d4))
(label concl4)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;IT WORKS
;time used: 110 ms
;after initialisation
; facts: (¬NATNUM(I) ¬NATNUM(N) ¬hf(M,N)=0∧¬hf(M,N)=1 ¬NATNUM(M) ¬MεStab1(N)
¬hf(N',M)=0 ¬K1<M ¬NATNUM(M) ¬MεStab1(N) ¬hf(N',M)=0 ¬K1<M
(¬NATNUM(J)∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N') ...)
;number of unifiable pairs: 19
;number of positive atoms: 7 and number of negative atoms: 18
;after first irrelevance elimination:
;time used: 14 ms
; facts: (¬MεStab1(N) ¬hf(N',M)=0 ¬K1<M ¬MεStab1(N) ¬hf(N',M)=0 ¬K1<M
(****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
¬MεStab1(N) ¬K<M JεStab1(N')∧I<J)
;number of unifiable pairs: 17
;number of positive atoms: 7 and number of negative atoms: 9
;time used: 21 ms
;after primitive propagation
;8 combination failures.
; facts: (¬MεStab1(N) ¬hf(N',M)=0 ¬K1<M ¬MεStab1(N) ¬hf(N',M)=0 ¬K1<M ¬MεStab1(N) ¬K<M
JεStab1(N')∧I<J (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N'))
;number of unifiable pairs: 17
;number of positive atoms: 7 and number of negative atoms: 9
;time used: 16 ms
;after propagation
;8 combination failures.
; facts: (¬MεStab1(N) ¬hf(N',M)=0 ¬K1<M ¬MεStab1(N) ¬hf(N',M)=0 ¬K1<M ¬K<M JεStab1(N')∧I<J
(****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N'))
;number of unifiable pairs: 16
;number of positive atoms: 7 and number of negative atoms: 8
;time used: 5 ms
;after noncyclicity marking
;number of cyclic conjunctions found: 0
;top-level unifiers: (2 2 2 2 2 2 1 3 2)
;***
;uniflst for ¬MεStab1(N)
;***
;path:
;KεStab1(N) from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
:: ¬MεStab1(N) from ¬MεStab1(N)
;unifier: ((K . M))
;path:
;N1εStab1(N) from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
:: ¬MεStab1(N) from ¬MεStab1(N)
;unifier: ((N1 . M))
;***
;uniflst for ¬hf(N',M)=0
;***
;path:
;hf(N',K)=0 from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
:: ¬hf(N',M)=0 from ¬hf(N',M)=0
;unifier: ((K . M))
;path:
;hf(N',N1)=0 from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
:: ¬hf(N',M)=0 from ¬hf(N',M)=0
;unifier: ((N1 . M))
;***
;uniflst for ¬K1<M
;***
;path:
;J<K from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N') ::
¬K1<M from ¬K1<M
;unifier: ((K . M) (K1 . J))
;path:
;I<J from JεStab1(N')∧I<J :: ¬K1<M from ¬K1<M
;unifier: ((J . M) (K1 . I))
;***
;uniflst for ¬MεStab1(N)
;***
;path:
;KεStab1(N) from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
:: ¬MεStab1(N) from ¬MεStab1(N)
;unifier: ((K . M))
;path:
;N1εStab1(N) from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
:: ¬MεStab1(N) from ¬MεStab1(N)
;unifier: ((N1 . M))
;***
;uniflst for ¬hf(N',M)=0
;***
;path:
;hf(N',K)=0 from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
:: ¬hf(N',M)=0 from ¬hf(N',M)=0
;unifier: ((K . M))
;path:
;hf(N',N1)=0 from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
:: ¬hf(N',M)=0 from ¬hf(N',M)=0
;unifier: ((N1 . M))
;***
;uniflst for ¬K1<M
;***
;path:
;J<K from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N') ::
¬K1<M from ¬K1<M
;unifier: ((K . M) (K1 . J))
;path:
;I<J from JεStab1(N')∧I<J :: ¬K1<M from ¬K1<M
;unifier: ((J . M) (K1 . I))
;***
;uniflst for ¬K<M
;***
;path:
;I<J from JεStab1(N')∧I<J :: ¬K<M from ¬K<M
;unifier: ((J . M) (K . I))
;***
;uniflst for JεStab1(N')∧I<J
;***
;path:
;JεStab1(N') from JεStab1(N')∧I<J :: ¬N1εStab1(N') from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
;I<J from S(N',J)∧I<J :: ¬K<M from ¬K<M
;unifier: ((N1 . M) (J . M) (K . I))
;path:
;JεStab1(N') from JεStab1(N')∧I<J :: ¬N1εStab1(N') from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
;I<J from JεStab1(N')∧I<J :: ¬K1<M from ¬K1<M
;unifier: ((N1 . M) (J . M) (K1 . I))
;path:
;JεStab1(N') from JεStab1(N')∧I<J :: ¬N1εStab1(N') from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1Stab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
;I<J from S(N',J)∧I<J :: ¬K1<M from ¬K1<M
;unifier: ((N1 . M) (J . M) (K1 . I))
;***
;uniflst for (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
;***
;path:
;JεStab1(N') from JεStab1(N')∧I<J :: ¬N1εStab1(N') from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
;hf(N',N1)=0 from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
:: ¬hf(N',M)=0 from ¬hf(N',M)=0
;N1εStab1(N) from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
:: ¬MεStab1(N) from ¬MεStab1(N)
;J<K from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N') ::
¬K1<M from ¬K1<M
;KεStab1(N) from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
:: ¬MεStab1(N) from ¬MεStab1(N)
;hf(N',K)=0 from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
:: ¬hf(N',M)=0 from ¬hf(N',M)=0
;unifier: ((J . M) (N1 . M) (K . M) (K1 . J))
;path:
;JεStab1(N') from JεStab1(N')∧I<J :: ¬N1εStab1(N') from
(****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
;hf(N',N1)=0 from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
:: ¬hf(N',M)=0 from ¬hf(N',M)=0
;N1εStab1(N) from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
:: ¬MεStab1(N) from ¬MεStab1(N)
;J<K from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N') ::
¬K1<M from ¬K1<M
;KεStab1(N) from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
:: ¬MεStab1(N) from ¬MεStab1(N)
;hf(N',K)=0 from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
:: ¬hf(N',M)=0 from ¬hf(N',M)=0
;unifier: ((J . M) (N1 . M) (K . M) (K1 . J))
;time used: 20 ms
;after finding a path
;path:
;I<J from JεStab1(N')∧I<J :: ¬K1<M from ¬K1<M
;JεStab1(N') from JεStab1(N')∧I<J :: ¬N1εStab1(N')
;from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
;hf(N',N1)=0 from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
:: ¬hf(N',M)=0 from ¬hf(N',M)=0
;N1εStab1(N) from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
:: ¬MεStab1(N) from ¬MεStab1(N)
;J<K from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N') ::
¬K1<M from ¬K1<M
;KεStab1(N) from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
:: ¬MεStab1(N) from ¬MεStab1(N)
;hf(N',K)=0 from (****∨KεStab1(N)∧hf(N',K)=0∧J<K)∧N1εStab1(N)∧hf(N',N1)=0∧¬N1εStab1(N')
:: ¬hf(N',M)=0 from ¬hf(N',M)=0
;unifier: ((K1 . I) (J . M) (N1 . M) (K . M) (K1 . J))
;deps: (A B4 D4 C4)
;time used: 415 ms
;after finding a path
;path:
;J<K0 from hf(0,K0)=0∧J<K0 :: ¬N1<MAX(N1,N2)' from ¬N1<MAX(N1,N2)'
;I<J from JεStab1(0)∧I<J :: ¬N2<MAX(N1,N2)' from ¬N2<MAX(N1,N2)'
;hf(0,K0)=0 from hf(0,K0)=0∧J<K0 :: ¬hf(0,MM(N,K1))=0 from (¬hf(0,MM(N,K1))=0∨¬K1<MM(N,K1))∧hf(0,N)=1∧¬NεStab1(0)
;hf(0,K0)=0 from hf(0,K0)=0∧J<K0 :: ¬hf(0,MAX(N,I)')=0 from ¬hf(0,MAX(N,I)')=0∧¬hf(0,MAX(N,I)')=1
;JεStab1(0) from JεStab1(0)∧I<J :: ¬NεStab1(0) from (¬hf(0,MM(N,K1))=0∨¬K1<MM(N,K1))∧hf(0,N)=1∧¬NεStab1(0)
;J<K0 from hf(0,K0)=0∧J<K0 :: ¬K1<MM(N,K1) from (¬hf(0,MM(N,K1))=0∨¬K1<MM(N,K1))∧hf(0,N)=1∧¬NεStab1(0)
;hf(0,N)=1 from (¬hf(0,MM(N,K1))=0∨¬K1<MM(N,K1))∧hf(0,N)=1∧¬NεStab1(0) :: ¬hf(0,MAX(N,I)')=1
from ¬hf(0,MAX(N,I)')=0∧¬hf(0,MAX(N,I)')=1
;bound in variable CTR85
;unifier: ((N . J) (I . I) (N2 . I) (N1 . J) (K0 . MAX(J,I)') (J . MAX(J,I)')
(N . MAX(J,I)') (K0 . MM(MAX(J,I)',J)) (K1 . J))
;deps: (A B1 C1)
(N . j)
(I . i)
(N2 . i)
(N1 . j)
(K0 . max(j,i)')
(J . max(j,i)')
(N . max(j,i)')
(K0 . mm(max(j,i)',j))
(K1 . j))
¬[N2<MAX(N1,N2)']
¬N2<MAX(N1,N2)'
::
;JεStab1(0) ;i<J from
from [hf(0,K0)=0∧j<K0] [JεStab1(0)∧i<J]
;hf(0,K0)=0 ;j<K0
:: :: ::
¬hf(0,mm(N,K1))=0 ¬K1<mm(N,K1) ¬NεStab1(0)
¬[¬(hf(0,mm(N,K1))=0∧K1<mm(N,K1)) ⊃(hf(0,N)=1⊃NεStab1(0))]
;hf(0,N)=1
::
¬hf(0,max(N,I)')=0 ¬hf(0,max(N,I)')=1
from ¬[hf(0,max(N,I)')=0∨hf(0,max(N,I)')=1]
::
;hf(0,K0)=0 ;j<K0
from [hf(0,K0)=0∧j<K0]
::
¬N1<MAX(N1,N2)'
from ¬[N1<MAX(N1,N2)']
;;;more sketches
(setq der-veryfast t)
(ekl)
(wipe-out)
(get-proofs minus prf ekl sys)
(proof foo)
(decl stabf (type: |ground→ground|))
(decl (hom1 Hom) (type: |ground→truthval|))
(axiom |∀x y.x≤max(x,y) ∧ y≤max(x,y)|)
(label max)
(assume |(∀X.stabf(X)=0∨stabf(X)=1)|)
(label a)
(assume |(∀X1.stabf(X1)=0∨stabf(X1)=1)|)
(label b)
(assume |∀Z1.(∃B10.∀y.hom1(y)∧stabf(y)=0⊃y≤B10) ⊃ (hom1(Z1)∧stabf(Z1)=1⊃Hom(Z1))|)
(label c)
(assume |∀Z2.¬((∃u.∀D10.hom1(D10)∧stabf(D10)=0⊃D10≤u)∧
(∃u.∀D11.hom1(D11)∧stabf(D11)=0⊃D11≤u)) ⊃ (hom1(Z2)∧stabf(Z2)=0⊃Hom(Z2))|)
(label d)
(assume |∀Z3.¬(∃u.∀D12.hom1(D12)∧stabf(D12)=0⊃D12≤u) ⊃ (hom1(Z3)∧stabf(Z3)=0⊃Hom(Z3))|)
(label e)
(assume |∀Z4.(∃B11.∀y.hom1(y)∧stabf(y)=0⊃y≤B11)∨
(∃B12.∀y.hom1(y)∧stabf(y)=0⊃y≤B12) ⊃ (hom1(Z4)∧stabf(Z4)=1⊃Hom(Z4))|)
(label f)
(assume |¬∃K10.∀x.Hom(x)⊃x≤k10|)
(label g)
(assume |¬∃K11.∀x.Hom(x)⊃x≤k11|)
(label h)
(assume |∃i.(∀J10.Hom(J10)⊃J10≤i)|)
(label i)
(derive |false| (a b c d e f g h i i i i))
(derive |¬∃i.∀J10.Hom(J10)⊃J10≤i|
(max a b c d e f g h i i i))
(setq der-slow t)
(fload padua)
(ekl)
(setq s:facts nil
g:split-equalities nil
g:time 0
g:decidingp t
g:report-time t
g:report-atoms t
g:report-facts t
g:report-unifiers t
g:report-top-uniflsts t
g:report-cycles t
g:decide-debugging t)
(setq s:facts nil
g:split-equalities nil
g:time nil
g:decidingp nil
g:report-time nil
g:report-atoms nil
g:report-facts nil
g:report-unifiers nil
g:report-top-uniflsts nil
g:report-cycles nil
g:decide-debugging nil)